the_es:ES, e:E, l:IdLnk. (haslnk(l;e))  ((isrcv(e)) c (lnk(e) = l)) 

latex

Definitions	x:A. B(x), P  Q, b, haslnk(l;e), A c B, p  q, if b then t else f fi , ff, t  T, P  Q, tt, P & Q, P  Q, True, , , Unit, False,
Lemmas	es-isrcv wf, bool wf, eqtt to assert, iff functionality wrt iff, assert wf, eq lnk wf, es-lnk wf, true wf, assert-eq-lnk, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, false wf, IdLnk wf, es-E wf, event system wf